updated lean symbol generation to be based on the npm package#338
updated lean symbol generation to be based on the npm package#338
Conversation
There was a problem hiding this comment.
Pull request overview
This PR migrates Lean Unicode symbol generation away from a vendored JSON file / GitHub download, and instead sources the abbreviation table from the pinned @leanprover/unicode-input npm package.
Changes:
- Remove committed/generated Lean symbol artifacts (
completions/symbols+lean.json,completions/lean-abbreviations.json) and ignore the generated output going forward. - Update
scripts/generate-symbols.mjsto read the Lean abbreviation table fromnode_modules/@leanprover/unicode-input. - Add
@leanprover/unicode-inputand wire symbol generation into the build vianpm run generate-symbolsand an updatedesbuildscript.
Reviewed changes
Copilot reviewed 5 out of 8 changed files in this pull request and generated 2 comments.
Show a summary per file
| File | Description |
|---|---|
| scripts/update-symbols.sh | Removed the old curl-based download script. |
| scripts/README.md | Updated symbol generation docs to reference npm-based source and new commands. |
| scripts/generate-symbols.mjs | Loads abbreviations from the npm package and uses robust path resolution. |
| package.json | Adds @leanprover/unicode-input, adds generate-symbols script, runs it before esbuild. |
| package-lock.json | Locks @leanprover/unicode-input@0.1.9. |
| completions/symbols+lean.json | Removed previously committed generated output. |
| completions/lean-abbreviations.json | Removed previously committed Lean abbreviation table. |
| .gitignore | Ignores generated completions/symbols+lean.json. |
💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.
| "vscode:prepublish": "npm run typecheck && npm run esbuild -- --minify --sourcemap=no", | ||
| "esbuild": "node esbuild.mjs", | ||
| "generate-symbols": "node scripts/generate-symbols.mjs", | ||
| "esbuild": "npm run generate-symbols && node esbuild.mjs", | ||
| "typecheck": "tsc -b", |
There was a problem hiding this comment.
completions/symbols+lean.json is now generated and gitignored, but npm run typecheck (and vscode:prepublish, which runs typecheck first) does not generate it. On a fresh clone/CI this will fail because editor/src/index.ts imports ../../completions/symbols+lean.json and the file won't exist yet. Fix by running generate-symbols before typecheck (e.g., make typecheck run npm run generate-symbols && tsc -b, or add a pretypecheck script; you may also want the same for lint if eslint resolves imports).
There was a problem hiding this comment.
Valid claim of the problem. I updated the typecheck script which seems to be the easiest solution. This does actually mean, that in case of the prepublish script we run it twice. But its fast and otherwise we have to change a lot more in the build process, where I think this is an okay tradeoff to make, but let me know if I should change it.
There was a problem hiding this comment.
I'm totally fine with running generate-symbols twice.
It is in my opinion a bit strange to have to run it before the typechecker.
@Tammo0987 Remark: Can we add a placeholder file, maybe? That way typechecking does not fail and we still build the file in the build step.
There was a problem hiding this comment.
I would actually argue against a placeholder file. Either we put in some wrong data in a placeholder file and then we actually miss very easily when we forgot to generate. Or we have the current generated one in there, but then it does not really make sense to let it be auto generated.
I think for the long run, the right solution should be, that we consolidate all of the npm build scripts, but we shouldn't do that here nor I know the constraints and requirements. So if you agree with that, you (or me) can merge it :)
There was a problem hiding this comment.
Right, let's keep it like this. Feel free to merge!
I think for the long run, the right solution should be, that we consolidate all of the npm build scripts, but we shouldn't do that here nor I know the constraints and requirements.
Let's maybe bring this up in the meeting as well.
DikieDick
left a comment
DikieDick
left a comment
There was a problem hiding this comment.
Neat!
Added one remark under one of Copilots comments.
Can be merged after discussing my remark :)
Description
In this issue I removed the lean abbreviations file and replaced by using it directly from the lean Unicode package. I updated all necessary scripts.
Testing this PR
Test the script by following the steps in scripts/README.md for the symbol generation. Possibly just run the project as well.
Closes #324